0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 9 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_AAG(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
APPEND3A_IN_AAG(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_AAG(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_AAG(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
APPEND3A_IN_AAG(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_AAG(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
append3A_in_aag([], T5, T5) → append3A_out_aag([], T5, T5)
append3A_in_aag(.(T10, []), T20, .(T10, T20)) → append3A_out_aag(.(T10, []), T20, .(T10, T20))
append3A_in_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → U1_aag(T10, T29, T33, T34, T32, append3A_in_aag(T33, T34, T32))
append3A_in_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63))) → U2_aag(T41, T60, T64, T65, T63, append3A_in_aag(T64, T65, T63))
U2_aag(T41, T60, T64, T65, T63, append3A_out_aag(T64, T65, T63)) → append3A_out_aag(.(T41, .(T60, T64)), T65, .(T41, .(T60, T63)))
U1_aag(T10, T29, T33, T34, T32, append3A_out_aag(T33, T34, T32)) → append3A_out_aag(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32)))
APPEND3A_IN_AAG(.(T10, .(T29, T33)), T34, .(T10, .(T29, T32))) → APPEND3A_IN_AAG(T33, T34, T32)
APPEND3A_IN_AAG(.(T10, .(T29, T32))) → APPEND3A_IN_AAG(T32)
From the DPs we obtained the following set of size-change graphs: